Nuprl Lemma : subtype-fpf-cap5 0,22

X:Type, eq:EqDecider(X), fg:x:X fp Type, x:Xf || g  f(x)?Void  g(x)?Top 
latex


Definitionsf || g, EqDecider(T), f(x)?z, Unit, P  Q, P & Q, x  dom(f), a:A fp B(a), , Prop, b, A, b, Top, f(x), xt(x), x:AB(x), P  Q, t  T
Lemmasfpf-ap wf, assert wf, not wf, bnot wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, top wf, fpf-cap wf, deq wf, fpf wf, fpf-compatible wf

origin